### Testing a generic term rewrite framework
#### Chris Eidhof, Sebastiaan Visser

**!
Automated testing using QuickCheck is a useful addition to Haskell's type
system. Both can be used to state important properties of code.  Manually
producing test data when dealing with a generic library defeats the purpose of
generic programming. We show how generic programming can be used to avoid the
boilerplate burden of automated testing.

@@ toc

*** Introduction

As part of the ongoing research on generic programming at the Center for
Software Technology a framework has been designed for generic term rewriting in
Haskell. This framework allows users to define rules which declare domain
specific semantic equivalences. These rules can be used to automatically
rewrite abstract syntax trees for arbitrary domains.

This paper starts by giving a simple introduction to the usage of the
framework. This is accompanied by a simple problem domain we use throughout the
entire paper. The second chapter describes some possible problems that can
arise when using the framework. The third chapter sketches how to prevent these
problems by using automated testing using QuickCheck Quickcheck. In the fourth
chapter we show how to implement a generic version of QuickCheck's arbitrary
function.  This function significantly decreases the amount of work that has to
be done in order to use automated testing.

*** Rewriting Expression

We can easily illustrate the use of this framework by means of an example.
Suppose that we are writing an interpreter or compiler for a simple logical
expression language. The data type for our expression language consists out of
constructors for the constants _true_ and _false_, the binary
operations for the logical _and_, _or_, _implication_ and
_bi-implication_, the _negation_ and _variables_:

@@ haskell

  data Logic =
       T
    |  F
    |  Logic :&&:   Logic
    |  Logic :||:   Logic
    |  Logic :->:   Logic
    |  Logic :<->:  Logic
    |  Not Logic
    |  Var String

Using this data type it is possible to express all sorts of logical statements:

@@ haskell

  (Var "x" :->: F) :&&: (Not T :||: Var "y")

  (T :<->: F) :->: (F :->: Var "x") :&&: T

  (F :||: T) :->: (T :||: F)

An evaluation function together with an variable environment can be used to
reduce these expressions to a single truth value. The following example shows
how to evaluate a logical statement using an simple environment.

@@ haskell

  expr = (Var "x" :->: F) :&&: (Not T :||: Var "y")

  eval [("x", False), ("y", True)] expr == True

*** Rewrite rules

Before the semantic interpretation of an expression it might be desirable to
perform some rewriting of the terms first. In general, term rewriting can be
used for several purposes. Dependent on the problem domain terms can be
rewritten in order to optimize, normalize or simplify the interpretation. As a
practical example, most modern compilers perform lots of rewrite rules to the
input program in order to simplify the compilation and produce efficient
machine code.

The rewrite framework allows us to express these rules and apply them to our
syntax trees. In order to demonstrate this, we show how to express three simple
logical equivalence rules. The first rule is the elimination of double
negations, the second and third are the well known De Morgan rules for
_or_ and _and_ respectively:

@@ haskell

  notNot      x   = Not (Not x)    |- x
  deMorganOr  x y = Not (x :||: y) |- Not x :&&: Not y
  deMorganAnd x y = Not (x :&&: y) |- Not x :||: Not y

Note how this code is the actual Haskell code -- and the _only_ Haskell
code -- that is needed to express these rules. The functions that express the
rules are parametrized with the meta-variables that connect the left hand side
with the right hand sides of the rule. The turnstile symbol ($\vdash$) can be
seen as the infix constructor for rules, taking two semantically equivalent
expressions. 

*** Rewrite function

To apply these rules the framework offers the function =rewrite=. This function
takes a rule and a term and rewrites the term using the rule. When the term
does not match the rule's left hand side the rewritten term equals the original.

@@ haskell
  rewrite :: PFView a => Rule a -> a -> a

The term will only be rewritten on the top level, it does not decent into the
term for deep application. To perform deep rewriting of terms the framework
offers the ability to express rewrite strategies. The explanation of strategies
is outside the scope of this paper.

  *** Representation

  So we can use the rewrite framework to easily apply term rewrite rules to our
  logical expression data type. The power of the framework can not only be
  found in ease of use, but also in the fact that it can be used for _any_
  data type. It uses generic programming to abstract over types.

  Because standard Haskell does not allow reflection over data types we have to
  supply the framework with a representation of our data type manually. We can
  get a rich set functions for free when we create a _generic view_, but
  creating such a view can be a tedious task. This can be illustrated with the
  clumsy piece of code in the [#PFView Logic|figure for the =Logic= instance
  for =PFView=].

  #anchor PFView Logic

    #caption The _structural representation_ for the =Logic= data type:

      @@ haskell

        instance PFView Logic where

          type PF Logic =
            C (Sum (Sum (Sum (Con (K String))   (Con (Prod Id Id)))
                        (Sum (Con (Prod Id Id)) (Con (Prod Id Id))))
                   (Sum (Sum (Con (Prod Id Id)) (Con Id))
                        (Sum (Con Unit)         (Con Unit))))

          from (Var x)     = C (Inl (Inl (Inl (Con "Var" (K x)))))
          from (p :<->: q) = C (Inl (Inl (Inr (Con "<->" (Prod (Id p) (Id q))))))
          from (p :->: q)  = C (Inl (Inr (Inl (Con "->"  (Prod (Id p) (Id q))))))
          from (p :&&: q)  = C (Inl (Inr (Inr (Con "&&"  (Prod (Id p) (Id q))))))
          from (p :||: q)  = C (Inr (Inl (Inl (Con "||"  (Prod (Id p) (Id q))))))
          from (Not p)     = C (Inr (Inl (Inr (Con "Not" (Id p)))))
          from T           = C (Inr (Inr (Inl (Con "T"   Unit))))
          from F           = C (Inr (Inr (Inr (Con "F"   Unit))))

          to (C (Inl (Inl (Inl (Con _ (K x))))))                = Var x
          to (C (Inl (Inl (Inr (Con _ (Prod (Id p) (Id q))))))) = p :<->: q
          to (C (Inl (Inr (Inl (Con _ (Prod (Id p) (Id q))))))) = p :->: q
          to (C (Inl (Inr (Inr (Con _ (Prod (Id p) (Id q))))))) = p :&&: q
          to (C (Inr (Inl (Inl (Con _ (Prod (Id p) (Id q))))))) = p :||: q
          to (C (Inr (Inl (Inr (Con _ (Id p))))))               = Not p
          to (C (Inr (Inr (Inl (Con _ Unit)))))                 = T
          to (C (Inr (Inr (Inr (Con _ Unit)))))                 = F

  This representation uses a common method in generic programming; the data
  type will be represented by making the sums, products, constructor names and
  fixed points explicit. The framework uses _type families_ to express the
  relation between the original type and the structural type. In this case the
  data type =Logic= and the structural representation =PF Logic=. The functions
  =from= and =to= form a so called _embedding projection pair_.  This pair
  can be used to convert values in the real world to and from the
  representation world.

*** Problems

Up till now we have introduced a generic term rewrite framework and
demonstrated how to use this for a simple logical expression language. Because
of the generality of the framework the usage was very simple. Despite this
simplicity, things can go wrong that the compiler will not notice. We isolate
three possible issues:

- The rewrite function works on every data type, this means the implementation
  must be very precise. How do we ensure that the algorithm is correct?

- For every data type that we want to apply a generic function to, we have to
  create a structural representation by hand. From the types of the
  representation we can easily see that the compiler cannot ensure us that
  there are no mistakes in the definition. How do we ensure that the
  representation is sound and complete? Can we check that the embedding
  projection pair forms a true isomorphism?

- When we rewrite a term using a rule we always assume that the semantics of
  the value do not change. How can we be sure that every rewrite rule is sound
  with respect to the semantics of the problem domain? In our case, are the
  left and right hand side of a rule semantically equivalent?

These three problems are very hard to tackle using Haskell's type system. We
have to find another way of ensuring ourselves the framework is applied
correctly.

*** Testing

Our solution to these potential problems is testing. We use QuickCheck to
automatically test the three properties. We can define a QuickCheck property
for all three problems and this way make sure the framework is used properly.

QuickCheck uses the =arbitrary= type class to create random instances of data
types as input for the tested properties. An instances for the =arbitrary=
class must to be specified for every data type you wish to test for.

Because we are dealing with a generic rewrite framework it would be rather
disappointing when users have to implement their =arbitrary= instances
manually. This is why we have chosen to generate these instance automatically
using a generic arbitrary function. This generic function can rely on the same
structural representation as the generic rewrite function.

  *** Rewrite property

  The rewrite property is used to test the correctness of the =rewrite= function.
  The property takes a rule and tests whether the rule is correctly applied to a
  random term. The term is randomly generated using the =arbitrary= class. The
  property plugs this term into the rule, rewrites the left hand side of the rule
  and compares this for equality with the right hand side of the rule.

  @@ haskell

    prop_rewrite :: PFView a => Rule a -> a -> Bool
    prop_rewrite rule a =
      rewrite rule (lhsR (rule a)) == rhsR (rule a)

  To test whether the rewrite algorithm works for the double negation rule we
  can write this:

  @@ haskell

    quickCheck (prop_rewrite notNot)

  Unfortunately there is currently no way to generate random rules in order to
  automate testing the rewrite property. For now it is sufficient to set up a
  number of test cases for some interesting rules. When the rewrite algorithm is
  implemented correctly, this test -- together with all other instances of this
  test -- should pass.

  *** View soundness

  As explained above, the user of the framework should manually supply a
  structural representation for their data type together with an embedding
  projection pair. Writing these instance becomes a real pain when data types
  grow bigger. Accidentally swapping a left projection with right projection in
  one of the arms of the embedding projection pair will not be noticed by the
  compiler and can cause serious problems.

  The following property should check the soundness of the =from= and =to=
  functions by checking whether they form the identity:

  @@ haskell

    prop_fromTo_Id :: PFView a => PF a -> Bool
    prop_fromTo_Id a = (from . to) a == a

  It is tempting to think that we could easily check for completeness by
  testing the isomorphism the other way around:

  @@ haskell

    prop_toFrom_Id :: PFView a => a -> Bool
    prop_toFrom_Id a = (to . from) a == a

  Actually -- in our framework -- this function will _not_ do the expected job.
  Because we generate the instances generically using the structural
  representation we are trying to test, the test depends on features we are
  currently testing! It is easy to see that without true reflection on data
  types generically testing for completeness is impossible. We might solve this
  problem in the future by automatically generating instances using techniques
  like Generic Haskell Generic Haskell or Scrap Your Boilerplate.

  As an example, the following QuickCheck property checks the soundness of the
  embedding projection pair for the =Logic= data type. When defined properly
  this test should pass.

  @@ haskell

    quickCheck (prop_fromTo_Id :: PF Logic -> Bool)

  *** Semantic soundness

  In order to test the semantic soundness of user defined rules we apply a
  trick quite similar to the one for the rewrite algorithm. Given a specific
  rule and a random term we fill in the meta-variable of the rule with this
  term. Now we rewrite the rule's left hand side and compare this for semantic
  equality with the right hand side. The property depends on a user defined
  function to test for domain specific semantic equivalence.

  @@ haskell

    prop_semantics :: PFView a =>
      (a -> a -> Bool) -> Rule a -> a -> Bool
    prop_semantics eq rule a =
      let lhs = lhsR (rule a)
      in maybe False (eq lhs) (rewriteM rule lhs)

  To demonstrate the usage of this property we give a specific instance of this
  property for the logical expression data type. This property check whether
  the original term and the rewritten term evaluate to the same value.

  @@ haskell

    prop_logicSemantics :: Rule Logic -> Logic -> Bool
    prop_logicSemantics = prop_semantics eqLogic
      where eqLogic a b = eval a == eval b

  As an example, the following property should pass for all instances of =x=.

  @@ haskell

    quickCheck
      $ prop_logicSemantics (\x -> x :||: Not x |- T))

*** Arbitrary instances

To use QuickCheck when testing properties, an instance of Arbitrary has to be
provided for every data type that is used. We will take a look at how this
instance is defined for a data type and then give a generic algorithm to
calculate them.

#caption The =Tree= data type:

  @@ haskell

    data Tree a =  Leaf a 
                |  Branch (Tree a) (Tree a)
       
First, let us look at the =Tree= data type in the figure. There is a
non-recursive constructor =Leaf= and a recursive constructor =Branch= that has
two fixed points, i.e. it recurses twice. The instance for =Arbitrary= is
defined as following:

@@ haskell

  instance Arbitrary a => Arbitrary (Tree a) where
    arbitrary = sized arbTree

  arbTree 0  =  Leaf <$> arbitrary
  arbTree n  =  frequency
    [  (1  ,  Leaf    <$>  arbitrary  )
    ,  (3  ,  Branch  <$>  arbTree    (n `div` 2) 
                      <*>  arbTree    (n `div` 2)) ]

The first thing to notice here is that we give a =sized= instance. This is
necessary for termination. If our size is =0=, we only generate the
non-recursive value =Leaf=. If the size is larger than =0=, we give each
constructor a weight of =1= plus the number of fixed points. Second, in the recursive
call, we divide the size by the number of fixed points for that constructor. This
way, the sized value will continue to decrease when recursing.

  *** Arbitrary instances: generically

  There are several aspects of the algorithm to calculate these instances
  generically. First, because our data types are represented as sums of
  products, we have to make the decision at every =Sum=. To get the frequencies
  for this decision, we have to synthesize the weights for both the left and
  the right subtree. Second, when recursing, we want to decrease the size by
  dividing it by the number of fixed points in the current constructor. This is
  number is also calculated in the =Sum= and passed on using the =divisor=
  field of =ArbParams=.

  #caption The function =garbitrary'= for the =GArbitrary= instance of =Sum f g=:

    @@ haskell

      garbitrary' params size  =  frequency 
        [(  fr fpl  ,  Inl   <$> garbitrary' params {divisor = sum fpl  } size)
        ,(  fr fpr  ,  Inr   <$> garbitrary' params {divisor = sum fpr  } size)
        ]
        where  
          (Node fpl fpr)  =   gfixpoints' (undefined :: Sum f g a)
          fr  ::  Tree Int -> Int
          fr  =   sum . fmap (freq size)
          freq  0  0  =  1 
          freq  0  _  =  0
          freq  _  x  =  x + 1

  In the figure, we see the code for the instance of =GArbitrary= for =Sum=. We
  call the =frequency= function with a list of two pairs, one for the =Inl= and
  one for the =Inr=. The first component of the pair is the frequency for that
  constructor, the second component is the recursive call for that sub-value.
  To calculate the frequency, we first calculate a binary tree that contains
  all the fixed points for every constructor, which has the same shape as the
  structural representation. The function =fr= calculates the frequency based
  on the size and the number of fixed points. If the size is =0=, it will only
  give non-recursive constructors a chance, otherwise we add =1= to the number
  of fixed points.

  There is one other interesting case for =GArbitrary=, and that is =Id=, which
  captures the recursion. Here we make use of the =ArbParams= data type, and use
  both the recursive call =r= and the divisor =d=:

  @@ haskell

    instance GArbitrary Id where
      garbitrary' p@(AP r d) size =
        Id <$> r p (size `div` d)

  For the full code of =GArbitrary=, see appendix~\ref{sec:garbitrary}.

  *** Calculating the fixed points

  For =garbitrary=, we need a tree of fixed points. Using the generic framework, we
  can calculate this. Our fixed points are stored in a binary tree with values at the
  leafs, just as in Figure~\ref{figure:treedt}.

  As an example, we want to calculate the fixpoint-tree for the =Direction=
  data type:

  @@ haskell

    data Direction  =  North  |  East
                    |  South  |  West
                    |  Direction :+: Direction

  The structural representation looks like this:

  @@ haskell

    type PF Direction =
          Sum  Unit 
               (Sum  Unit 
                     (Sum  Unit 
                           (Sum Unit (Prod Id Id))))

  There are two fixed points in the =:+:= constructor, and that is reflected in
  the structural representation by =Prod Id Id=. We can see the outcome of our
  algorithm in the figure.

  Our class for calculating the fixed points looks like this:

  @@ haskell

    class GFixpoints f where
      gfixpoints' :: f a -> Tree Int

  The value =f a= is never used directly in our instances, but is only provided
  so we can give inline types to our recursive calls, as we will see in the
  instance for =Sum=.

  For =Unit= and =K=, we return a singleton tree with =0= as the value. For the
  recursive calls, however, we need to return =1=:

  @@ haskell

    instance GFixpoints Id where
      gfixpoints' _ = Leaf 1

  For sum, we use =undefined= to make sure the recursive calls are on the
  components of =Sum=. In =garbitrary=, this is where we need to choose, so that
  is why we branch our tree here using =Node=.

  @@ haskell

    instance (  GFixpoints f, GFixpoints g) => 
                GFixpoints (Sum f g) where
      gfixpoints' _ =  gfixpoints' (undefined :: f a  )
               `Node`  gfixpoints' (undefined :: g a  )

  For =Prod=, we need to sum the values for both components. In the case of
  direction, we have a =Prod Id Id=. Calculating an =Id= value will return a =Leaf
  1=, and here we sum them to get a =Leaf 2=.

  @@ haskell

    instance (  GFixpoints f, GFixpoints g) =>
                GFixpoints (Prod f g) where
      gfixpoints' _ = (+)  <$>  gfixpoints' (undefined :: f a  )
                           <*>  gfixpoints' (undefined :: g a  )

  The full code for the GFixpoints module is in appendix~\ref{sec:gfixpoints}

*** Conclusion

We have seen how we can test our rewriting framework on the correctness of the
rewriting algorithm, how we can test our embedding projection pairs on
soundness and how we can test the rewriting rules on semantic equality. In
order to do this, we have shown a generic algorithm for creating QuickCheck
instances.

While we can currently only check for soundness of the embedding projection
pairs, we would ideally also test for completeness. This could be done by
introspection on the data type by, for example, using the Scrap Your
Boilerplate approach that is integrated in GHC. Alternatively we could use
Template Haskell, but the current implementation of Template Haskell does not
support type families.

We now have a powerful test framework that will catch a lot of mistakes,
automatically. For users of this test framework, a minimal amount of work has
to be done. They only have to make sure they test their rules with
=prop_semantics=.

*** Acknowledgements

We would like to thank the teachers and fellow students of the Generic
Programming course for the fun and insightful discussions during the course.
Also, Alexey Rodriguez deserves special mentioning, without his help and
encouragement this paper would not have been possible.

*** Appendices

  *** Module GArbitrary

  @@ haskell

    instance Applicative Gen where
      (<*>) = ap
      pure  = return

    data ArbParams a = AP {
        rec     :: ArbParams a -> Int -> Gen a
      , divisor :: Int
      }

    class GArbitrary f where
      garbitrary' :: ArbParams a -> Int -> Gen (f a)

    instance GArbitrary Unit where
      garbitrary' _ _ = pure Unit

    instance GArbitrary Id where
      garbitrary' p@(AP r d) t = Id <$> r p (t `div` d)

    instance Arbitrary a => GArbitrary (K a) where
      garbitrary' _ _ = K <$> arbitrary

    instance (GFixpoints f, GFixpoints g,
              GArbitrary f, GArbitrary g) =>
              GArbitrary (Sum f g) where
      garbitrary' p s = frequency [rec fpl Inl, rec fpr Inr]
        where
          rec a b =
            (fr a, b <$> garbitrary' p {divisor = sum a} s)
          (Node fpl fpr) = gfixpoints' (undefined :: Sum f g a)
          fr    = foldTree (f s) (+)
          f 0 0 = 1
          f 0 _ = 0
          f _ x = x + 1

    instance (GArbitrary f, GArbitrary g) =>
              GArbitrary (Prod f g) where
      garbitrary' p s = Prod <$>
        garbitrary' p s <*> garbitrary' p s

    instance GArbitrary f =>
      GArbitrary (Con f) where
      garbitrary' p s = Con "" <$> garbitrary' p s

    instance GArbitrary f =>
      GArbitrary (C f) where
      garbitrary' p s = C <$> garbitrary' p s

    garbitrary :: (GArbitrary (PF a), PFView a) =>
      Int -> Gen a
    garbitrary s = garbitraryHelper (AP undefined 1) s

    garbitraryHelper ::
      (PFView a, GArbitrary (PF a)) => 
      ArbParams a -> Int -> Gen a
    garbitraryHelper p s = to <$>
      garbitrary' p {rec = garbitraryHelper} s

  *** Module GFixpoints

    #anchor Module GFixpoints

    @@ haskell

      module GFixpoints where

      data Tree a = Leaf a | Node (Tree a) (Tree a)
       deriving Show

      instance Applicative Tree where
        pure = Leaf
        Leaf x <*> Leaf y = Leaf (x y)
        -- Partial instance.

      foldTree :: (a -> b) -> (b -> b -> b) -> Tree a -> b
      foldTree l n (Leaf x)   = l x
      foldTree l n (Node x y) =
        (foldTree l n x) `n` (foldTree l n y)

      sum :: Tree Int -> Int
      sum = foldTree id (+)

      instance Functor Tree where
        fmap f = foldTree (Leaf . f) Node

      class GFixpoints f where
        gfixpoints' :: f a -> Tree Int

      instance GFixpoints Unit where
        gfixpoints' _ = Leaf 0

      instance GFixpoints Id where
        gfixpoints' _ = Leaf 1

      instance GFixpoints (K a) where
        gfixpoints' _ = Leaf 0

      instance (GFixpoints f, GFixpoints g) =>
        GFixpoints (Sum f g) where
        gfixpoints' _ =
          gfixpoints' (undefined :: f a) `Node` gfixpoints' (undefined :: g a)

      instance (GFixpoints f, GFixpoints g) =>
                GFixpoints (Prod f g) where
        gfixpoints' _ = (+)  <$> gfixpoints' (undefined :: f a)
                             <*> gfixpoints' (undefined :: g a)

      instance GFixpoints f => GFixpoints (Con f) where
        gfixpoints' _ = gfixpoints' (undefined :: f a)
